*****∀E sknpk RW;

1 A(RW,RW,S,0)⊃∃w1.(A(RW,w1,P,0)∧¬agree(RW,w1))  

*****∀E reflex RW,S,0;

2 A(RW,RW,S,0)  

*****⊃E ↑↑,↑;

3 ∃w1.(A(RW,w1,P,0)∧¬agree(RW,w1))  

*****∃E ↑ w1;

4 A(RW,w1,P,0)∧¬agree(RW,w1)  (4)

*****∀E agree RW,w1;

5 agree(RW,w1)≡(M(RW)=M(w1)∧N(RW)=N(w1))  

*****∀E initial2 RW,w1;

6 (A(RW,RW,SP,0)∧A(RW,w1,P,0))⊃(M(w1)*N(w1))=(M(RW)*N(RW))  

*****∀E reflex RW,SP,0;

7 A(RW,RW,SP,0)  

*****∀E ok2 w1;

8 ok(M(w1),N(w1))  

*****TAUT ok(M(w1),N(w1))∧((M(w1)*N(w1))=(M(RW)*N(RW))∧¬(M(RW)=M(w1)∧N(RW)=N(w1))) 4:8;

9 ok(M(w1),N(w1))∧((M(w1)*N(w1))=(M(RW)*N(RW))∧¬(M(RW)=M(w1)∧N(RW)=N(w1)))  (4)

*****SUBST rw1 IN ↑;

10 ok(M(w1),N(w1))∧((M(w1)*N(w1))=(m0*N(RW))∧¬(m0=M(w1)∧N(RW)=N(w1)))  (4)

*****SUBST rw2 IN ↑;

11 ok(M(w1),N(w1))∧((M(w1)*N(w1))=(m0*n0)∧¬(m0=M(w1)∧n0=N(w1)))  (4)

*****∃I ↑ N(w1)←n M(w1)←m;

12 ∃m n.(ok(m,n)∧((m*n)=(m0*n0)∧¬(m0=m∧n0=n)))  

*****ASSUME ok(m,n)∧(m+n)=(m0+n0);

13 ok(m,n)∧(m+n)=(m0+n0)  (13)

*****SUBSTR rw1 IN ↑;

14 ok(m,n)∧(m+n)=(M(RW)+n0)  (13)

*****SUBSTR rw2 IN ↑;

15 ok(m,n)∧(m+n)=(M(RW)+N(RW))  (13)

*****∀E sknpk w;

16 A(RW,w,S,0)⊃∃w1.(A(w,w1,P,0)∧¬agree(w,w1))  

*****∀E initial3 RW,m,n;

17 (A(RW,RW,SP,0)∧(ok(m,n)∧(M(RW)+N(RW))=(m+n)))⊃∃w1.(A(RW,w1,S,0)∧(M(w1)=m∧N(w1)=n))  

*****∀E reflex RW,SP,0;

18 A(RW,RW,SP,0)  

*****TAUTEQ ∃w1.(A(RW,w1,S,0)∧(M(w1)=m∧N(w1)=n)) 15:18;

19 ∃w1.(A(RW,w1,S,0)∧(M(w1)=m∧N(w1)=n))  (13)

*****∃E ↑ w;

20 A(RW,w,S,0)∧(M(w)=m∧N(w)=n)  (20)

*****TAUT ∃w1.(A(w,w1,P,0)∧¬agree(w,w1)) 16,20;

21 ∃w1.(A(w,w1,P,0)∧¬agree(w,w1))  (20)

*****∃E ↑ w1;

22 A(w,w1,P,0)∧¬agree(w,w1)  (22)

*****∀E agree w,w1;

23 agree(w,w1)≡(M(w)=M(w1)∧N(w)=N(w1))  

*****∀E initial2 w,w1;

24 (A(RW,w,SP,0)∧A(w,w1,P,0))⊃(M(w1)*N(w1))=(M(w)*N(w))  

*****∧E 20:#1;

25 A(RW,w,S,0)  (20)

*****∀E sp1 RW,w,0;

26 (A(RW,w,S,0)∨A(RW,w,P,0))⊃A(RW,w,SP,0)  

*****TAUT (M(w1)*N(w1))=(M(w)*N(w)) 22:26;

27 (M(w1)*N(w1))=(M(w)*N(w))  (20 22)

*****∀E ok2 w1;

28 ok(M(w1),N(w1))  

*****∧E 20:#2;

29 M(w)=m∧N(w)=n  (20)

*****∧E ↑:#1;

30 M(w)=m  (20)

*****∧E ↑↑:#2;

31 N(w)=n  (20)

*****TAUT ¬(M(w)=M(w1)∧N(w)=N(w1)) 22:23;

32 ¬(M(w)=M(w1)∧N(w)=N(w1))  (22)

*****∧I ((28 27 32));

33 ok(M(w1),N(w1))∧((M(w1)*N(w1))=(M(w)*N(w))∧¬(M(w)=M(w1)∧N(w)=N(w1)))  (20 22)

*****SUBSTR 30 IN ↑;

34 ok(M(w1),N(w1))∧((M(w1)*N(w1))=(m*N(w))∧¬(m=M(w1)∧N(w)=N(w1)))  (20 22)

*****SUBSTR 31 IN ↑;

35 ok(M(w1),N(w1))∧((M(w1)*N(w1))=(m*n)∧¬(m=M(w1)∧n=N(w1)))  (20 22)

*****∃I ↑ N(w1)←n1 M(w1)←m1;

36 ∃m1 n1.(ok(m1,n1)∧((m1*n1)=(m*n)∧¬(m=m1∧n=n1)))  (13)

*****⊃I 13⊃↑;

37 (ok(m,n)∧(m+n)=(m0+n0))⊃∃m1 n1.(ok(m1,n1)∧((m1*n1)=(m*n)∧¬(m=m1∧n=n1)))  

*****∀I ↑ m n;

38 ∀m n.((ok(m,n)∧(m+n)=(m0+n0))⊃∃m1 n1.(ok(m1,n1)∧((m1*n1)=(m*n)∧¬(m=m1∧n=n1))))  

*****∃E nsk w;

39 A(RW,w,S,0)∧¬agree(RW,w)  (39)

*****∀E agree RW,w;

40 agree(RW,w)≡(M(RW)=M(w)∧N(RW)=N(w))  

*****TAUT ¬(M(RW)=M(w)∧N(RW)=N(w)) 39:40;

41 ¬(M(RW)=M(w)∧N(RW)=N(w))  (39)

*****∀E initial1 RW,w;

42 (A(RW,RW,SP,0)∧A(RW,w,S,0))⊃(M(w)+N(w))=(M(RW)+N(RW))  

*****∀E reflex RW,SP,0;

43 A(RW,RW,SP,0)  

*****∀E ok2 w;

44 ok(M(w),N(w))  

*****TAUT ok(M(w),N(w))∧((M(w)+N(w))=(M(RW)+N(RW))∧¬(M(RW)=M(w)∧N(RW)=N(w))) 39:44;

45 ok(M(w),N(w))∧((M(w)+N(w))=(M(RW)+N(RW))∧¬(M(RW)=M(w)∧N(RW)=N(w)))  (39)

*****SUBST rw1 IN ↑;

46 ok(M(w),N(w))∧((M(w)+N(w))=(m0+N(RW))∧¬(m0=M(w)∧N(RW)=N(w)))  (39)

*****SUBST rw2 IN ↑;

47 ok(M(w),N(w))∧((M(w)+N(w))=(m0+n0)∧¬(m0=M(w)∧n0=N(w)))  (39)

*****∃I ↑ N(w)←n M(w)←m;

48 ∃m n.(ok(m,n)∧((m+n)=(m0+n0)∧¬(m0=m∧n0=n)))